//MAX-SAT problem-depended class
//$Id: maxsat.h 612 2010-11-28 18:40:53Z Oleg.Bulychov $
#pragma once

#include "src/heo/include/lf_endl.h"
#include "src/heo/include/random.h"
#include "src/heo/include/calc_hash.h"
#include "src/heo/include/reflection.h"
#include "src/heo/include/transmit_array.h"
#include "src/heo/include/solution.h"
#include "src/heo/include/optimization_direction.h"

struct MaxSat_Config
{
    double      initial_probability_;
    int         limit_output_;

    static char const* get_Name() { return "maxsat"; }
    static char const* get_Section() { return get_Name(); }

    template<class V>
    void accept(V& v)
    {
        v(VAR_(initial_probability),        0.5);
        v(VAR_(limit_output),               20);
    }
};

struct MaxSat_Problem
{
    typedef int size_type;
    //:typedef uint64_t size_type;

    int                 dimension_;
    size_type           clause_count_;
    int                 min_clause_size_;
    int                 max_clause_size_;
    std::vector<int>    data_;

    explicit MaxSat_Problem():
        dimension_(0),
        min_clause_size_(std::numeric_limits<int>::max()),
        max_clause_size_(0)
    {}

    static char const* get_Default_File_Name() { return "sample.cnf"; }

   /* The file can start with comments, that is lines beginning with the character 'c'.
      Right after the comments, there is the line "p cnf nbvar nbclauses" indicating that
      the instance is in CNF format; nbvar is the number of a variables appearing in the file;
      nbclauses is the exact number of clauses contained in the file.
      Then the clauses follow. Each clause is a sequence of distinct non-null numbers between
      -nbvar and nbvar ending with 0 on the same line. Positive numbers denote the corresponding
      variables. Negative numbers denote the negations of the corresponding variables.
    */
    template<class I, class E>
    bool read(I& in, E* env, random_generator& rnd)
    {
        std::string s;
        for (;;)
        {
            in >> s;
            if ("c" == s)
            {
                in.skipline();
                continue;
            }
            else
                break;
        }
        if (s != "p")
            return false;
        in >> s;
        if (s != "cnf")
            return false;
        uint64_t clause_count;
        in >> dimension_ >> clause_count;
        if (dimension_ <= 0 || clause_count <= 0)
            return false;
        VERIFY_(clause_count <= (uint64_t)std::numeric_limits<size_type>::max());//:see above
        clause_count_ = (size_type)clause_count;
        data_.reserve(3 * clause_count_);
        int k = 0;
        for (size_type i = 0; i < clause_count_; ++i)
        {
            int j = 0;
            size_t n = data_.size();
            data_.push_back(0);
            ++k;
            for (;; ++j, ++k)
            {
                int lit;
                in >> lit;
                if (!lit)
                    break;
                if (Abs(lit) > dimension_)
                    return false;
                data_.push_back(lit);
            }
            if (j <= 0 || j > dimension_)
                return false;
            data_[n] = j;
            if (j > max_clause_size_)
                max_clause_size_ = j;
            if (j < min_clause_size_)
                min_clause_size_ = j;
        }
        return true;
    }
};
//__________________________________________________________________________________
//__________________________________________________________________________________
class MaxSat_Solution
{
    //DISALLOW_COPY_AND_ASSIGN(MaxSat_Solution);
public:
    typedef maximization<> TDirection;
    typedef int            TCostType;
protected:
    Array<bool>     data_;
    TCostType       cost_;
    bool            changed_;
    unsigned        hash_;
    bool            hash_changed_;
public:
    explicit MaxSat_Solution():
        data_(),
        cost_(),
        changed_(),
        hash_(),
        hash_changed_()
    {}

    template<class E>
    void init(E* env, random_generator& rnd)
    {
        size_t dim = env->problem_.dimension_;
        data_.set_Size(dim);
    }

    template<class E>
    void generate(E* env, random_generator& rnd)
    {
        for (size_t i = 0; i < data_.size(); ++i)
        {
            bool f = rnd.next_Double() < env->cfg_.initial_probability_;
            data_[i] = f;
        }
        changed_ = true;
    }

    TCostType get_Cost() const
    {
        ASSERT_(!changed_);
        return cost_;
    }

    unsigned get_Hash()
    {
        ASSERT_(!changed_);
        if (hash_changed_)
        {
            hash_changed_ = false;
            hash_ = Calc_Hash(&data_[0], data_.size() * sizeof(data_[0]));
        }
        return hash_;
    }

    template<class E>
    void evaluate(E* env, random_generator& rnd)
    {
        if (!changed_)
            return;
        changed_ = false;
        hash_changed_ = true;
        TCostType f = 0;
        int const* clause = &env->problem_.data_[0];
        for (MaxSat_Problem::size_type i = 0; i < env->problem_.clause_count_; ++i)
        {
            int clause_length = *clause++;
            for (int j = 0; j < clause_length; ++j)
            {
                int lit = clause[j];
                if (lit < 0)
                {//!x 
                    if (!data_[-lit - 1])
                    {
                        ++f;
                        break;
                    }
                }
                else
                {//x
                    if (data_[lit - 1])
                    {
                        ++f;
                        break;
                    }
                }
            }
            clause += clause_length;
        }
        cost_ = f;
    }

    template<class V>
    void accept(V& v)
    {
        v(cost_);
        v(changed_);
        v(data_);
        v(hash_);
        v(hash_changed_);
    }

    template<class T>
    void assign(T const& t)
    {
        ASSERT_(data_.size());
        ASSERT_(data_.size() == t.data_.size());
        size_t size = data_.size();
        for (size_t i = 0; i < size; ++i)
        {
            data_[i] = t.data_[i];
        }
        changed_        = t.changed_;
        cost_           = t.cost_;
        hash_           = t.hash_;
        hash_changed_   = t.hash_changed_;
    }

    template<class X>
    void copy_To(X& x) const
    {
        x.assign(*this);
    }

    template<class E>
    void print(std::ostream& os, E* env)
    {
        for (int i = 0; i < (int)data_.size(); ++i)
        {
            os << (data_[i] ? i + 1 : -i - 1) << " ";
            if (i > env->cfg_.limit_output_)
            {
                os << "...";
                break;
            }
        }
        os << lf
            << "cost: " << get_Cost() << lf
            << "clauses: " << env->problem_.clause_count_ << lf
            << "not satisfied: " << env->problem_.clause_count_ - get_Cost() << lf;
    }

    template<class E>
    static bool read(E* env, std::string const& file_name, Solution_Pool<MaxSat_Solution>& pool)
    {
        //:see onemax.h for example
        return false;
    }

    template<class E>
    void write(E* env, std::string const& file_name, size_t id, size_t count)
    {
        //:see onemax.h for example
    }
};
//__________________________________________________________________________________
//__________________________________________________________________________________
//__________________________________________________________________________________

//EOF!
